Nuprl Lemma : append_iseg
11,40
postcript
pdf
T
:Type,
as
,
bs
,
cs
:(
T
List). iseg(
T
; append(
as
;
bs
); append(
as
;
cs
))
iseg(
T
;
bs
;
cs
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
append(
as
;
bs
)
,
prop{i:l}
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
,
P
Q
,
P
Q
,
iseg(
T
;
l1
;
l2
)
,
||
as
||
Lemmas
append
assoc
,
append-cancellation
,
length
wf1
,
append
wf
origin
T:Type, as,bs,cs:(T List). iseg(T; append(as; bs); append(as; cs)) 
iseg(T; bs; cs) T:Type, as,bs,cs:(T List). iseg(T; append(as; bs); append(as; cs)) iseg(T; bs; cs) 
Tx:A. B(x)
x:A. B(x) Q Q
Q Q